等価制約,Coercible, 種制約
等価制約
コンテキストは,t1 ~ t2という形式の等価制約を含むことができ,これはt1とt2の型が同じである必要があることを表す記法である.型族の存在下では,2つの型が等しいかどうかは一般に,局所的には決定できない.したがって,関数の型シグネチャの型クラス制約には,次の例のように等価制約が含まれることがある.
code:ec01.hs
sumCollects :: (Collects c1, Collects c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
ここで,c1とc2の要素の型が同じであることを要求している.一般に,等価制約の型t1とt2は任意の単型(monotype)であってよい.つまり,高ランク型が有効であるかどうかにかかわらず,いかなる量化子も含んではならないということである.
等価制約は,型クラスおよびインスタンスのコンテキストにも現れる.前者は,関数従属を使っているプログラムを,代わりにシノニム族を使っているプログラムに変換できるようにする.要するに,次の形式のクラス宣言を
code:ec02.hs
class C a b | a -> b
以下のように書き換えるということでである.
code:ec03.hs
class (F a ~ b) => C a b where
type F a
つまり,我々はすべての関数従属(FD)a1 .. an -> bをFD型族F a1 ..と親クラスのコンテキストの等価性F a1 .. an ~ bによって表し, 本質的には関数従属に名前を与えていることになる.クラスインスタンスでは,クラス宣言の先頭に従ってFD型族の型インスタンスを定義する.メソッドの型シグネチャはそのプロセスの影響を受けない.
Heterogeneous equality
GHCはまた,2つの潜在的に異なる種を持つ型を関連付ける,kind-heterogeneous equalityもサポートしている.heterogeneous equalityは~~と書かれる.これらの違いをよりよく理解するために,以下に~と~~の種を与える.
code:ec04.hs
(~) :: forall k. k -> k -> Constraint
(~~) :: forall k1 k2. k1 -> k2 -> Constraint
ユーザはおそらく~を欲しがちだが,GHCが演繹的に2つの型の関心が同じ種であることを知ることができなければ~~が有用である.(a :: k1) ~~ (b :: k2)であるという証拠は,k1とk2が同じで,aとbが同じであることをGHCに伝える.
~の方がよりcommonなequality relationなので、GHCは-fprint-equality-relationsがセットされていない限り~~を~のようにプリントアウトする.
Unlifted heterogeneous equality
GHCの内部には,さらに第3の等式関係 (~#) がある.これは(~~のように)heterogeneousであり,GHC内部でのみ使われる.エラーメッセージやその他の出力に表示されるのは,-fprint-equality-relationsが有効になっている場合だけである.
Coercible制約
制約Coercible t1 t2はt1 ~ t2と同様であるが,役割(Role)の文脈におけるt1とt2の間のrepresentational equality を表す記法である.これはData.Coerceによってエクスポートされる(Data.Coerceにはドキュメンテーションも含まれている).より多くの詳細と議論は論文 “ Safe Coercions”にある.
制約種
ConstraintKinds
7.4.1以降
Constraint種を持つ型をコンテキストで使用できるようにする.
通常,制約(型の中で=> 矢印の左側に表れるもの)の構文は非常に制限されており,以下のパターンしかない.
型クラス制約.例えば Show aなど.
Implicit parameter制約.例えば ?x::Intなど(ImplicitParams拡張を伴って).
等価制約.例えばa 〜 Int など(TypeFamiliesまたはGADTs拡張を伴って).
ConstraintKinds拡張を使うと,GHCはあなたのプログラムの中で制約として受け入れるものにおいてより自由になる.正確には,このフラグがあれば,新たな種Constraintに属する任意の型を制約条件として使用することができる.次のようなものはConstraint種を持つ.
フラグなしの制約ですでに有効なものすべて.具体的に言えば,完全適用された型クラス,Implicit Parameter,等価制約のこと.
すべてのコンポーネント型がConstraint種のタプル.例えば(Show a, Ord a) 型はConstraint種を持つ.
その形式がまだ知られていないものの,ユーザがConstraint種を持つと宣言したもの(宣言するにはGHC.ExtsからConstraintをインポートする必要がある).例えばtype Foo (f :: Type -> Constraint) = forall b. f b => b -> bは許され,また型族を含む以下の例も同様に許される.
code:ec05.hs
type family Typ a b :: Constraint
type instance Typ Int b = Show b
type instance Typ Bool b = Num b
func :: Typ a b => a -> b -> b
func = ...
制約は特定の種を持つ型として扱われているだけなので,この拡張では型制約シノニムを使用できることに留意せよ.
code:ec06.hs
type Stringy a = (Read a, Show a)
foo :: Stringy a => a -> (String, String -> a)
foo x = (show x, read)
現在,インスタンスのコンテキストおよび親クラスでは,標準の制約,タプル,およびこれら2種類の制約に対する型シノニムのみが許可されている(追加のフラグなし).その理由は,次の2つのプログラムのように,より一般的な制約を許可すると型チェックがループする可能性があるためだ.
code:ec07.hs
type family Clsish u a
type instance Clsish () a = Cls a
class Clsish () a => Cls a where
code:ec08.hs
class OkCls a where
type family OkClsish u a
type instance OkClsish () a = OkCls a
instance OkClsish () a => OkCls a where
インスタンスのコンテキストや親クラスでエキゾチックな制約を使用するプログラムを書くこともできるがそうするためには、型検査器が終了しなくても気にしないことを示すためにUndecidableInstancesを使用する必要がある.